% Based on our experience, we discuss the strengths and limitations of the
% studied approach.
% We demonstrated how automated, semi-formal verification can be useful for
% verifying industrial transformations. We claim that this approach is transferrable to other
% industrial transformations after incorporating some changes into the
% verification tool. For example, pruning the state space to remove any classes or
% transformation rules that are not involved in the constraint being verified will
% shorten the execution time of the verification tool. We also claim that
% automatically verifying rule-based transformations is easier than automatically
% verifying Java transformations. (To Fabian) Discuss in what ways is it
% different; formulation of the invariants - carrying out the actual verification/proof - how
% in rule based transformations you can prove an invariant for the entire transformation , not
% just on one of its rules (This is almost impossible in Java) etc.
% On the other hand, several issues present threats to the validity of our case
% study. First, although the case study investigates a transformation that
% manipulates large industrial metamodels, transformations that cover the entire
% metamodels (not just a subset of the metamodels) should also be investigated so
% that an informed conclusion can be made on the practicality of using such tools
% in industry. Second, the verification prototype can only handle non-recursive,
% purely declarative transformations. To be readily adaptable in industry,
% verification prototypes are needed that can reason about turing-complete
% transformations developed using different constructs (e.g. imperative or
% functional constructs). Finally, although the automated verification approach
% helped in uncovering bugs in an industrial transformation, the verification is not
% completely formal and the results only hold for a bounded search space. On
% the other hand, formal verification tools can prove properties for any
% search space size but are more difficult to implement and use. Thus, more
% research is needed to identify the trade-offs in using formal verification and
% automated, semi-formal verification for industrial transformations.
% \begin{itemize}
%   \item verification is not fully formal + invariants hold for search space of a
%   specific size
%   \item Prototype verifes declarative transformations only. Further, prototype
%   considers certain kinds of transformations. I.e. we only handle non recursive
%   transformations (we handle lazy rules but not if they call each other). So
%   prototype can verify transformations expressed in non-turing complete
%   (subsets of) languages.
%   \item We used a big model transformation in the sense that the used metamodels
%   are big, however the rules donot cover the entire metamodels. Bigger,
%   industrial transformations are needed to prove the scalability of the used
%   verification approach 
% \end{itemize}